$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $x$, $y$:$A$, $v$:Top. $x$ $\in$ dom($y$ : $v$) $\sim$ (eqof(${\it eq}$)($y$,$x$))